Runtime Complexity (innermost) proof of /tmp/tmpSh6-R5/Liveness6.3.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

↳2 CdtProblem

↳3 CdtUnreachableProof (⇔)

↳4 CdtProblem

↳5 CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication)

↳6 CdtProblem

↳7 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))

↳8 CdtProblem

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳10 CdtProblem

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳12 CdtProblem

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳14 CdtProblem

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳16 CdtProblem

↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳18 CdtProblem

↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳20 CdtProblem

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳22 CdtProblem

↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳24 CdtProblem

↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳26 CdtProblem

↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳28 CdtProblem

↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳30 CdtProblem

↳31 SIsEmptyProof (⇔)

↳32 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(bot) → c3(SENT(bot))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))

S tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(bot) → c3(SENT(bot))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))

K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, TOP, CHECK

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(bot) → c3(SENT(bot))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))

S tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(bot) → c3(SENT(bot))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))

K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c3, c4, c5, c6, c10, c11, c12, c13, c14, c, c1, c2

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 12 dangling nodes:

REC(bot) → c3(SENT(bot))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))

S tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))

K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c12, c13, c14, c, c1, c2

(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(no(z0)) → c14(NO(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [4]
POL(NO(x₁)) = 0
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [3] + [3]x₁
POL(no(x₁)) = [4] + [5]x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = [2]x₁
POL(up(x₁)) = [5]

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(up(z0)) → c10(CHECK(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [5] + [4]x₁
POL(NO(x₁)) = 0
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [3]x₁
POL(no(x₁)) = [2]x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [1] + x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REC(up(z0)) → c4(REC(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [5]
POL(NO(x₁)) = 0
POL(REC(x₁)) = [4]x₁
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [5]x₁
POL(no(x₁)) = [3]x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [1] + x₁

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

NO(up(z0)) → c6(NO(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [3] + x₁
POL(NO(x₁)) = [2]x₁
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = x₁
POL(no(x₁)) = [4]x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [1] + x₁

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [5] + x₁
POL(NO(x₁)) = 0
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [2] + [3]x₁
POL(no(x₁)) = [1] + x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [1] + x₁

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [2] + [3]x₁
POL(NO(x₁)) = [2]
POL(REC(x₁)) = [2]x₁
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [5] + [4]x₁
POL(no(x₁)) = [1] + [2]x₁
POL(rec(x₁)) = [4]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [1] + x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [2] + [2]x₁
POL(NO(x₁)) = [5]
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [3] + [3]x₁
POL(no(x₁)) = [4] + [5]x₁
POL(rec(x₁)) = [4] + [4]x₁
POL(sent(x₁)) = [5] + x₁
POL(up(x₁)) = [4] + x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(rec(z0)) → c12(CHECK(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [2] + [4]x₁
POL(NO(x₁)) = [4]
POL(REC(x₁)) = 0
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [4]x₁
POL(no(x₁)) = [1] + [2]x₁
POL(rec(x₁)) = [4] + [3]x₁
POL(sent(x₁)) = x₁
POL(up(x₁)) = [5] + x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))
REC(rec(z0)) → c(REC(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REC(rec(z0)) → c(REC(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [2]
POL(NO(x₁)) = 0
POL(REC(x₁)) = [2]x₁
POL(SENT(x₁)) = 0
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [2] + [3]x₁
POL(no(x₁)) = [2] + x₁
POL(rec(x₁)) = [4] + [4]x₁
POL(sent(x₁)) = [5] + x₁
POL(up(x₁)) = [4] + x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(27) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [5] + [2]x₁
POL(NO(x₁)) = [2]
POL(REC(x₁)) = [2]x₁
POL(SENT(x₁)) = [3]
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = [2] + [3]x₁
POL(no(x₁)) = [4] + x₁
POL(rec(x₁)) = [4] + [4]x₁
POL(sent(x₁)) = [5] + x₁
POL(up(x₁)) = [4] + x₁

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:

SENT(up(z0)) → c5(SENT(z0))

K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SENT(up(z0)) → c5(SENT(z0))

We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
sent(up(z0)) → up(sent(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)
no(up(z0)) → up(no(z0))

And the Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHECK(x₁)) = [3] + [4]x₁
POL(NO(x₁)) = 0
POL(REC(x₁)) = [4]x₁
POL(SENT(x₁)) = [3] + x₁
POL(bot) = [4]
POL(c(x₁)) = x₁
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(check(x₁)) = x₁
POL(no(x₁)) = [3] + [4]x₁
POL(rec(x₁)) = [4] + [3]x₁
POL(sent(x₁)) = [4] + [2]x₁
POL(up(x₁)) = [1] + x₁

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0))
rec(sent(z0)) → sent(rec(z0))
rec(no(z0)) → sent(rec(z0))
rec(bot) → up(sent(bot))
rec(up(z0)) → up(rec(z0))
sent(up(z0)) → up(sent(z0))
no(up(z0)) → up(no(z0))
top(rec(up(z0))) → top(check(rec(z0)))
top(sent(up(z0))) → top(check(rec(z0)))
top(no(up(z0))) → top(check(rec(z0)))
check(up(z0)) → up(check(z0))
check(sent(z0)) → sent(check(z0))
check(rec(z0)) → rec(check(z0))
check(no(z0)) → no(check(z0))
check(no(z0)) → no(z0)

Tuples:

REC(up(z0)) → c4(REC(z0))
SENT(up(z0)) → c5(SENT(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
CHECK(no(z0)) → c14(NO(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))

S tuples:none
K tuples:

CHECK(no(z0)) → c14(NO(z0))
CHECK(up(z0)) → c10(CHECK(z0))
REC(up(z0)) → c4(REC(z0))
NO(up(z0)) → c6(NO(z0))
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0))
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0))
CHECK(rec(z0)) → c12(CHECK(z0))
REC(rec(z0)) → c(REC(z0))
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0))
SENT(up(z0)) → c5(SENT(z0))

Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c12, c

(31) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtUnreachableProof (EQUIVALENT transformation)

(4) Obligation:

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

(6) Obligation:

(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(10) Obligation:

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(12) Obligation:

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(14) Obligation:

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(16) Obligation:

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(18) Obligation:

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(20) Obligation:

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(22) Obligation:

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(24) Obligation:

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(26) Obligation:

(27) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(28) Obligation:

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(30) Obligation:

(31) SIsEmptyProof (EQUIVALENT transformation)

(32) BOUNDS(O(1), O(1))